Land native Effect/ST and record the 2026-10-17 scoreboard - #145

A rank-n dictionary field quantifies its own variables, so those variables
do not make the record's layout depend on a free type variable. Parameter
shapes then use the same scalar layout as other closed records instead of
the erased aggregate special case.

PSRS_DUMP_CC and PSRS_DUMP_WAT write the calling-convention and text
forms beside a focused runtime test without changing the compiled artifact.

The vendored official `Safe.Coerce` shadows the compiler's primitive
interface for the same module. Its body is `coerce = unsafeCoerce`, whose
`unsafeCoerce` is a self-recursive stub this project cannot execute, so every
program that reaches it loops at runtime.

Keep the vendored source faithful to upstream and resolve the module through
the compiler interface instead: expose `compiler_provided_module` from
`psrs-resolve` and have the driver's library loader skip such a name.
Imports then fall through to the virtual interface, which maps `coerce` to the
checked coercion intrinsic and `Coercible` to the shared class.

`Unsafe.Coerce` has no compiler interface yet; its `foreign import` is
represented as the same recursive stub, so a program that reaches it is a
recorded gap rather than a working coercion.

The live-type layout filter added when the core libraries were vendored only
lays out arrays and records reachable from a declaration or constructor field,
so the raw-type layout fixtures never reserved their aggregates. Root those
types through declarations in the tests, which is what the production builder
sees.

Split `psrs-ast/tests.rs` and `psrs-typecheck/classes/fundeps.rs` into module
directories; both crossed the 500-line source limit earlier on this branch.

An abstract constructor application (`f a`, including `f Unit`) lowers to an
erased value whose stored calling convention is established by its producer.
Recovering it at a concrete consumer needs that convention; the previous code
cast the erased closure directly onto the consumer signature, which trapped
when a dictionary method produced a closure under its own protocol
(`wasm trap: cast failure`).

Add read-only checked instantiation evidence (`psrs-core`), a shared
conversion planner that recovers the producer protocol and emits an explicit
adapter when it differs from the consumer (`cc/lower/conversion`), and thread
the evidence to each boundary (global use, direct call, dictionary field,
erased local use). The Effect representation owner contributes its runtime
token as the `Effect` constructor protocol. A reference cast is no longer used
as an adapter, and a missing constructor binding is a source-spanned
unsupported conversion rather than a fresh guess.

Value-sensitive Wasmtime execution now covers the non-Effect Reader
dictionary, Effect discard, delayed map, and a fixed `f Unit` payload, plus
signature inspection of the generated adapter and factory. Ordinary closure
and aggregate regressions are re-run through the workspace suite.

PE-13 and EF-14 are recorded as verified in the acceptance documents.

A callee that is not a top-level declaration - a local closure or a class
method reached through a field access - was rejected when under-applied
(`call expects N arguments but received M`). Only top-level declarations had
a partial-application path.

Add `lower_indirect_partial_application`: evaluate the callee and the supplied
arguments, capture them, and emit a generated closure that exposes the
remaining parameters and calls the captured callee indirectly. The generated
closure is verified like any other function before it is added.

Cover both an under-applied local closure and an under-applied dictionary
method with Wasmtime execution.

The L6/M7 scoreboard moved from 207/413 to 210/413: three corpus cases whose
first blocker was P8 closure conversion now run. D-04 and README are updated.

The runtime-representation model and checked-boundary contract was spread
across the erasure and aggregate documents and referenced by name from several
topics, so each feature grew its own notion of how a value is adapted. Give it
a single owner, name it after industry practice, and make the target layout a
total level of the same model.

- New functional topic representation-and-evidence.md: the target-neutral
  RuntimeRep (the analogue of GHC's RuntimeRep), RepresentationPolicy, Boundary,
  Evidence, ConversionPlan, generic aggregate normalization and the aggregate
  conversion plan, the representation owners, and the one planner. A RuntimeRep
  a target uses has exactly one Layout, joined by a total mapping per target
  (heap_layout for Wasm GC; abi_layout for the Canonical ABI), which is what
  makes the functional backend complete. Erasure, callables, dictionaries,
  effects, coercion, and partial application become instances of it in their own
  documents, deferring to it instead of restating it.
- data-representation is named as the Wasm GC heap_layout realization of each
  RuntimeRep, with a total ValueShape -> ValueType mapping; the former
  generic-aggregate-erasure design is folded into the model (normalization and
  conversion) and this document (layouts).
- Erasure defines the policy of an erased value and its ownership (producer),
  grounded in GHC RuntimeRep/Any, Swift reabstraction thunks and witness
  tables, and Java bridge methods.
- cc-ir: partial application is the standard PAP closure for every callee kind;
  the adapted function boundary is a reabstraction thunk; checked instantiation
  evidence travels through an explicit Core-to-CC side table.
- effects: the token is the State# RealWorld analogue; i32 0 is a placeholder
  and an implementation gap.
- modules-and-resolution, prim: coerce and unsafeCoerce are compiler-provided
  primitive values; a compiler-provided module is never shadowed.
- DEC-17 records the durable decision; the backend index and IR boundaries
  reference the new topic and name the evidence/policy side table.
- Acceptance records name the transitional mechanism and its removal target.

Replace the transitional representation mechanisms with the boundary the
design names. Checked instantiation evidence and each constructor's
representation policy now travel to P8 through BoundaryEvidence beside CC,
the same discipline ExternalBindings uses for WIT bindings.

- Add RepresentationRegistry: Function stores under its checked
  instantiation arguments; the trusted Effect owner registers its runtime
  token. An unregistered constructor is reported, not resolved by arity.
- Intern one payload-erased protocol signature per registered callable
  constructor, keyed by the concrete signature, replacing the signature-prefix
  derivation in cc/layout/functions.
- Delete FunctionLowerer::source, constructor_protocols,
  transport_signatures, protocol_parameters, and cc/lower/instantiation.rs.
- Route every use (global, direct call, dictionary field, erased local) through
  BoundaryEvidence.

Behaviour is unchanged: the focused closure_protocol, partial_application,
effects, and functor cases pass, and the driver suite stays at 549 passed/10
pre-existing failures.

Register Unsafe.Coerce in the compiler-provided interface and the
unsafeCoerce intrinsic in the compiler vocabulary, so the vendored module
is never loaded and its self-recursive body never takes effect.

- Add Intrinsic::UnsafeCoerce with the forall a b. a -> b scheme.
- Infer it as an unconstrained coercion function (no Coercible wanted);
  finalize closes it to a THIR UnsafeCoerce node lowered to Core's
  RepresentationCast.
- Lower the intrinsic in CC through the common conversion planner, so it
  reinterprets the value at the erased boundary.
- Add execution evidence (newtype through unsafeCoerce) plus the
  compiler-spelling scope test.

The driver suite stays at 551 passed/10 pre-existing failures.

Replace the transitional Int token and its i32 0 placeholder with the
compiler-owned opaque state token the design names (the State# RealWorld
analogue). Effect lowering interns TypeId::STATE_TOKEN, marks it opaque,
and threads it through each Effect closure; run supplies the StateToken
value instead of an Int literal.

- Add TypeId::STATE_TOKEN and Core ExprKind::StateToken. Only effect
  lowering produces it; the Core verifier requires it to carry the
  compiler token type, and the backend lowers it to a scalar constant
  because the synchronous effect carries no payload.
- Update every Core traversal to treat the token as a leaf.
- Update the effect fixture and the model, effects, and acceptance notes.

The driver suite stays at 551 passed plus one pre-existing prim_row
failure; the scoreboards are unchanged (L1 904/908, L2 71/72 + 386/413,
L3 39/48, L4 39/50, L5 58/81, L6/M7 210/413).

The matching module had two relation-shaped methods, subsumes and matches,
with no single entry point. Fold them into one checked relation,
TypeMatcher::relate(actual, expected, variance, instantiate), parameterized
by Variance::{Subsumption, Invariant}. Subsumption is the value-level
relation a scheme is checked against at its use; Invariant is the rigid
mode for nominal and higher-kinded applications, closed and rigid rows,
and constructor field templates.

This is a behaviour-preserving structural change: every recursion and entry
point now goes through relate, and the two modes keep their exact branch
logic. The public entry points (compatible, scheme_instance,
application_matches, instantiation) are unchanged. Checking remains the
sole owner of the relation; P8 consumes only its Instantiation evidence.

Validated: psrs-core, psrs-typecheck, and the full driver suite (551 passed,
same 10 pre-existing failures) are unchanged, and all five scoreboards are
unchanged (L1 904/908, L2 71/72 + 386/413, L3 39/48, L4 39/50, L5 58/81,
L6/M7 210/413).

A constructor field whose immediate head is a type variable, such as `f a`,
is compared through the class's higher-kinded counterpart `eq1`/`compare1`
instead of requiring `Eq (f a)`/`Ord (f a)`. This is upstream's
`isAppliedVar` test in TypeChecker/Deriving.hs, and the vendored
Data.Functor.App, Compose, Coproduct, and Product declarations rely on it.

`Eq1` and `Ord1` now derive as `eq1 = eq` and `compare1 = compare`,
matching upstream's deriveEq1 and deriveOrd1, so the matching `Eq`/`Ord`
instance supplies the dictionary.

The `Data.Foldable` graph no longer stops on `no instance for constraint
Eq (_ _)` or `Ord (_ _)` in those modules.

A class-method use that is not applied, such as `eq = eq1` or
`compare = compare1`, kept its method-local `forall` and constraints on the
inferred type. Checking it against the plain function type the instance method
expects then reported a type mismatch instead of providing the method's
dictionary.

The expected-type path now runs the inferred expression through the shared
`instantiate_expression_use`, the same operation the application path already
uses, so the method-local obligation becomes a wanted constraint. This lets
Data.Functor.Product and Data.Functor.Coproduct's hand-written `eq = eq1`
and `compare = compare1` type check.

…l classes

Compiler-supported deriving is now its own topic: it selects rules from one
registry built once from the resolved declarations, validates each field's
usage and variance against the visible instance environment, and reports the
official deriving errorCode for every failure.

The known classes are no longer recognized by comparing class module and name
strings at use time. DerivingRegistry maps resolved class identities to their
methods, to the representation declarations (Data.Ordering, Data.Generic.Rep),
and to the trusted core values (append, mempty, identity, apply, pure) the fold
and traversal rules name. A Newtype/Generic trailing wildcard is resolved to
the wrapped type or representation before the instance is recorded, so the
searchable head is concrete.

usage.rs walks each field with polarity and instance existence, so a field head
with no mapping instance is rejected at the declaration with
CannotDeriveInvalidConstructorArg, matching purs. Every structural class now has
a rule: Eq/Ord/Eq1/Ord1, Functor/Bifunctor/Contravariant/Profunctor,
Foldable/Bifoldable, Traversable/Bitraversable, Newtype, Generic, and derive
newtype. Eq and Ord normalize field synonyms before the applied-variable test.

The new diagnostics map to their official codes: CannotDerive,
ExpectedTypeConstructor, InvalidDerivedInstance, InvalidNewtypeInstance,
CannotDeriveNewtypeForData, CannotDeriveInvalidConstructorArg,
CannotFindDerivingType, and ExpectedWildcard. derive newtype on a data type is
InvalidNewtypeInstance, and deriving the Newtype class for a data type is
CannotDeriveNewtypeForData, as purs reports.

Deriving is documented as its own topic and split out of FE-16 into FE-22.

Validated: psrs-typecheck 134 passed; the deriving source tests 16 passed, the
runtime deriving tests 8 passed under PSRS_REQUIRE_WASMTIME=1, and the upstream
deriving batteries 2 passed (18 accept/reject cases and an errorCode
comparison). The full driver suite is 561 passed with the same 10 pre-existing
failures. Traversable/Bitraversable execution is blocked by a P8 CC
verification limit and is recorded as such.

Ordinary Coercible still cannot lift Coercible a b through an unknown
constructor to Coercible (f a) (f b). That refusal matches purs.
derive newtype does not ask for the proof. After the local single-field
newtype and the underlying instance are checked, the derived methods reuse
the wrapped dictionary and adapt each boundary with a representation cast
authorized by that newtype.

Beta-reducing the cast kept the method quantifier only on the let result.
The binding now carries the same leading forall, so a variable such as
Traversable's m stays in scope. The quantifier is not Coercible evidence.

Validated with focused driver tests under PSRS_REQUIRE_WASMTIME=1,
including unknown-constructor dictionary reuse, the ordinary Coercible
rejection, and derived Traversable execution. The psrs-core optimizer
tests passed. The full workspace suite was not run.

A record constructor or updater with an immediate underscore becomes a
lambda whose binders follow the written fields, not the canonical field
order. Nested update paths share that updater. An explicit field
expression or nested literal keeps its own scope, so
`field = field { value = 7 }` uses the local `field` value. AST updates
now distinguish a nested path from an expression, and resolution projects
the path from the enclosing base.

A parenthesized backticked section accepts the hole on either side and
keeps the operand order and the unresolved local name.

Validated under PSRS_REQUIRE_WASMTIME=1: the record suite (21) and the
backticked-section test. The full workspace suite was not run.

An applied foreign import data value is not a nullary handle and has no
constructors. Closure conversion gives it the same non-null erased reference
as an abstract type variable, so a saturated Fn2 can pass layout.

An underscore written as the condition, then branch, or else branch becomes
a parameter in that order, the same way a case scrutinee already does.

A value signature depends on the type constructors and classes that remain
after a saturated local synonym expands. Constructor fields count only for
the constructors the export actually lists.

A.zip between backticks is that qualified value used infix, so both operands
stay on the operator chain.

A synonym consumes only its declared parameters. Further arguments apply to
the expanded body, so C2 a z x is (C2 a z) x.

0xFFFF fits in Int. A magnitude at or above 0x80000000 remains IntOutOfRange.

A signed declaration solves every constraint, so a where-bound function quantified its monad before a use could refine that monad. A constraint stays on the local scheme only when that binding's type determines it. A constraint that still mentions an outer unknown stays with the enclosing declaration.

A fallthrough helper is defined in the same let as the case, so it can name an outer local directly. Passing that local in as a value argument instantiated its scheme once, before the guard applied the arguments that solve its constraints.

enumFromThenTo feeds Int to a locally generalized stepper and maps the result with toEnum. The same shape, including guards, operators, and composition, has to keep that seed as Int.

The native Effect/ST design's first implementation step is to validate the
shared representation and typed requests before migrating public modules. This
adds that prototype as a compiler regression test: a rank-N request functor
preserves a cell's element type, operand, and continuation result without a GADT
or an unsafe cast, and a free computation over it is interpreted one request at
a time with a tail-recursive interpreter.

The test compiles an Int cell and a String cell in one `do` program, writes both
in place, reads both, reads the WASI monotonic clock through a Host request
performed by the interpreter from a raw host leaf, and executes to 42.

It also records the design's flagged role risk as a real blocker: a free
computation whose `a` sits inside the request functor's parameter infers a
nominal result role, so the official `type role Effect representational` (which
ST.Global.toEffect relies on) cannot hold. The Host family, the facade newtype,
and the interpreter work and return 42; the public-module migration waits on
fixing the representation's result role. The ST facade, region boundary, Global
conversion, and public migration remain outstanding.

…boration

Share dispatch, execution, observable-event and owned-resumption relations across CC and MIR, with path-sensitive provenance and publication checks. Validate lifecycle bodies and total-call assumptions, and move cost probes after compiler verification.

Add permanent malformed-IR and runtime regression coverage, align the control-machine design, and record remaining acceptance work and validation in the handoff.

Validation: control 185 passed, backend 444 passed, mandatory control integration 81 passed. Workspace snapshot retains the same 71 baseline failures. Formatting passes; strict Clippy remains blocked by the existing let_and_return warning.

P8 lowering, layout planning and every verifier inferred machine cases,
fields and helper roles from positional offsets. Add one stage-independent
named schema (control/schema.rs) and a frozen per-module placement
(cc/control/schema.rs, RepresentationTable::control_schema) that layout,
generation and verification consume. Positional case/field literals and
role-from-signature inference are replaced by named queries.

Replace the ad-hoc executor coverage set with a named ActionId registry whose
complete inventory must be observed. Add DEC-21, which resolves the
construction/verification boundary: a checked P8 plan expanded to ordinary
CC, with ordinary P9/P10 trusted under IR-invariant and behavior evidence.

Behavior is unchanged: focused control 185 passed, backend 445 passed.

P8 emitted every machine body as ordinary CC and the CC/MIR recognizers
recovered its meaning afterwards. Introduce a temporary checked construction
plan in cc/lower/control/plan/: named operands, selected cases, ordered
projections/allocations/applications/helper calls and one terminal Advance,
Publish, Return, Tail or Reject. `check`/`verify_plan` validate dispatch tag
validity, node arity and the complete ActionId inventory; `Machine::expand`
emits the same ordinary CC from the checked structure.

Every machine body now comes from a plan: the executor and the replay
(clone/rebuild), lifecycle (start/check/close), one-shot (once/cancel) and
raw-resume bodies. A test-gated bounded model compares each plan's terminal
traces against a table written from the operational semantics.

The CC and MIR machine-semantic recognizers are retired and replaced by boundary
checks: `cc::verify_module` compares each emitted CC body's dispatch and outcome
shape with the checked plan, and `mir::verify_module` compares each machine
function's dispatch arm set and non-self tail-call targets with the plan (self
tail calls loopify into back-edges and are excluded). cc/verify/control/* and
mir/control/* are deleted, MIR keeps only the helper call binding contract, and
the shared control/ relation layer is removed down to the named schema and the
ActionId inventory.

Assurance tradeoff recorded in the handoff: the boundary checks cover dispatch
coverage and external tail targets, not operand semantics, so IR-valid mutations
injected after construction are no longer rejected and the negative driver tests
that exercised them were removed with their modules. The handoff is updated as
the current snapshot with next actions.

Evidence: backend 454, focused control 10, eleven integration targets 82;
cargo test --workspace has only the pre-existing unrelated psrs-cli link
failure. Each file stays under the 500-line limit.

Add Run as the 40th ActionId with a straight-line checked plan: empty
queue, fresh Start, one root as both execution extent and dispatch
context, Close after Executor. Split the bounded model and CC operand
boundary into focused modules. P8 rejects host-handle captures in
control callbacks; P9 rejects nested canonical borrow captures.
RepresentationTable construction goes through from_parts so fixtures
cannot omit the frozen control schema.

Permanent regressions cover Root Start arity, exclusive-run sharing,
checkpoint and replay field roles, Bind/Resume/Finish construction,
foreign capture, instance-terminal traps, and GC-preserved array/string
buffers. control_reference permanently runs the locked Run/Row fixtures.
The 185 retired recognizer names are mapped as a requirement audit.

AE-01–AE-10 and AC-01–AC-05 are Verified on 2026-10-15. AE-11 remains
open. D-04 was not remeasured.

Evidence: focused control_regressions, backend lib including the model
and borrowed-handle tests, eleven integration targets 83,
control_reference 6, purs 0.15.16 control-types 17/17. Workspace and
scoreboards were not rerun.

The naive `Return`/`Suspend` free monad infers a nominal result role, so
the official `type role Effect representational` is RoleMismatch. Store
the result as phantom `Val` in a Free view and keep NativeF answer-indexed.
Prototype Effect and ST wrappers share that field; `toEffect` is
unsafeCoerce.

runNative reads the request payload and follows the Free continuation.
Abort is a Unit thunk so a strict interpreter record does not trap every
run. The prototype stays outside the package.

Evidence: RoleMismatch on the naive encoding; official Effect/ST roles
accepted; runST and toEffect/runEffect return 42 for Int/String cells plus
the monotonic clock. D-04 was not remeasured. AE-11 remains Unverified.

The standard library commit 4c73aab52226e8f5e7b1f17052f1a19d717a472e adapts
official Effect and ST onto PSRS.Effect.Native. This compiler change is the
tree that compiled and executed that package: generic command-runner
checking, rank-N specialization, WIT import schemes as layout roots, hidden
ST and Effect constructors, and the native representation driver.

stdlib.lock.json now names that package commit. The content fingerprint
remains fnv1a64-v1:ad19620ada1d2ecf. NE-01–NE-13 and AE-11 are Verified.
checkThrows, Console timers, Effect.Exception, and Effect.Aff stay
unimplemented. D-04 stays at 164/413 because the scoreboard was not
remeasured. The workspace suite was not rerun.

Evidence: native-effect 13/13, native-uncurried 21/21, native-types 11/11,
and the filtered identity/host driver run 3 passed. P8 rejects
unsafeCoerce 1 :: Ref Int before codegen.

L1–L4 stay at 904/908, 72/72 with passing resolution 403/413, 39/48, and
39/50. L5 moves from 75/97 to 77/97 because NoInstanceFound moves from
46/53 to 48/53. L6/M7 moves from 164/413 to 273/413. All 273 agreeing
cases exit 0, and none trap.

The other 140 are 69 library-foreign link failures, 34 P5 typecheck, 13
P8 closure conversion, 11 P5 kind check, 6 P3, 4 P0, one P7 command-runner
mismatch, one 10-second timeout, and BigFunction.purs, which the OS kills
before a diagnostic. The single-process board was killed the same way, so
the 412 completed cases each ran in their own scoreboard process against
the vendored corpus on Wasmtime 49.0.3.

The branch was not merged.

The execution workflow failed because the runner has no sibling
psrs-stdlib package. It now checks out the private biuld/psrs-stdlib
repository at the revision in stdlib.lock.json.

Prelude no longer exports runEffect. The official Effect runner is
Effect.Unsafe.unsafePerformEffect, and the seed still exits 42.

Nine modules were past 500 lines or shared a name with a directory.
Module roots now live in mod.rs, and the two over-limit functions
moved into focused submodules.

Official Prelude does not export Effect. These programs import it and
compile through the configured command runner. Binding lineage is now
observed on external-binding extraction, which replaced the old effect
lowering pass.

A push to an open pull-request branch also matches pull_request, so
the same commit ran cargo test --workspace twice. Pushes now run only
on master; pull requests keep the single required check.

The Core dump also names functor variables f. The old slice took the
first match and stopped after 4000 characters, before this
declaration's dictionary parameter.